Nuprl Lemma : delta_wf
11,40
postcript
pdf
i
,
j
:
. delta(
i
;
j
)
{0..2
}
latex
Definitions
False
,
P
Q
,
A
,
A
B
,
P
&
Q
,
i
j
<
k
,
delta(
i
;
j
)
,
{
i
..
j
}
,
t
T
,
x
:
A
.
B
(
x
)
,
Lemmas
le
wf
,
int
seg
wf
,
eq
int
wf
,
ifthenelse
wf
origin
i, j:
. delta(i;j) 
{0..2
} i, j:. delta(i;j) {0..2} 
Q
A
B j < k} Tx:A. B(x)